So actually, given that we are starting to narrow down to allied troops, maybe let me

make sure who has not seen those things before. Who has seen those things before? I have this

tendency to ask negative questions. Kind of, but it's not quite... Okay, no, then maybe

I'm not wasting my time today because if I knew that I can start going quicker, I would

prepare more material. But okay. So let us briefly recall where the motivation comes

from. I wrote all those equivalences that you don't have to parse yet. But I was trying

to suggest that they are meant to propagate, that they are meant to describe somehow inductively

or recursively the working of most of the connectives in terms of just this next step

for every immediate successor or for some immediate successor relation. And as I said,

it seems that somehow in a certain sense of being defined, other connectives can be defined

using this strange kind of equations. Even this is not exactly the kind of definition

or equivalence that we're talking so far. Maybe we need to make this idea more precise.

So I... This is redundant. This actually we can leave out and just keep S here only. So

as I said, we want to have a way to solve systems of equations of a certain kind. And

I left it a bit vague, or more than a bit vague, what I exactly meant by this. I was

just hinting that it will have to do in the end right now with computing denotations of

formulas on the model, which is really the whole point of doing model checking algorithms.

But in fact, the basic mathematics that I want to talk about will be applicable in much

broader context. So this is a bit vague in production. And let me now make more precise

what I want to talk about. So before we continue, I want to tell you a few words mathematically

about fixed points. And it is going to be useful not only for model checking, it will

be also useful later in semantics of programming languages. So this is why I feel excused to

scare you with a bit more mathematics and blackboard derivations. But this is very simple

mathematics. It's not going below undergraduate level in discrete math, let's say. So first

of all, recall the concept of preorder or quasi-order. Who knows what it is? Really,

you haven't seen this name? Preorder, quasi-order, Visek mandas of Deutsch. So one can see both

names being used in the literature. They are not introduced in glowing. They are not, okay,

so this is just a reflexive and transitive relation, okay? So there's something that

you have seen even if you didn't see the name, you have seen it and you work with it. Is

this clear what this means? So okay, maybe let's start with absolute. Sorry? Half or

no? That's consigned. I can only take over for this. Okay, so let us recall first of

all what is a relation and this is something that we have already said. So let W or S be

any set, let's start with W. So let W be any set. Relation on it. This we know, right?

Cartesian product and I think I already said it twice during this lecture. So what it means

for this thing to be reflexive? This must have been glowing. And for all V, V is in this relation

of itself, right? So another way of writing this is that this pair V, V belongs to this,

but this looks a bit funny, right? Anyway, set theoretically, this is what the relation

is. Who can help me? What shall I write? We have seen the definition of transitive relation.

So there are many situations in which such relations arise in nature. I'm tempted for

those of you who are in the mathematics, I can even point out the important subclass

of topologies. Alexander of topologies is yet another way of seeing them, but let's

start with something much more element, with much more obvious description. And we have

moreover a notion of partial order, which is pre-order or quasi-order, which just happens

to be antisymmetric. Is this notion clear? So antisymmetry means that if you have this

and if you have this, then you also have that. Then you already have the W is 2. OK, just

a mathematical definition like any other. There are some other variants of this notion,

like asymmetry, where you say that it cannot be the case that this and this hold at the

same time. So asymmetry is like a strict version of this weak ordering. So sometimes this can

be called weak partial order because this also, as I said, we have that every element

is comparable. And sometimes what is the name that is also used is when you're thinking